Example 4.4 in [Lucas - ICALP'96]

Summary: Ex4_4_Luc96b

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (Polynomials @ MuTerm)
  2. Giesl and Middeldorp's transformation (Metacombination @ AProVE)
  3. Polynomials (MuTerm)
  4. CSRPO
  5. CSDP

CS-TRS Ex4_4_Luc96b (file Ex4_4_Luc96b.csr)

Functions:  f g

Constructors:  g

Variables:  X Y

Arities: 

ar(f) = 2
ar(g) = 1

Replacement map: 

µ(f)={1}
µ(g)={1}

Rules: (file Ex4_4_Luc96b)

f(g(X),Y) -> f(X,f(g(X),Y))

The CS-TRS in OBJ format (file Ex4_4_Luc96b.obj):

obj Ex4_4_Luc96b is
  sort S .
  op f : S S -> S [strat (1 0)] .
  op g : S -> S .
  vars X Y : S .
  eq f(g(X),Y) = f(X,f(g(X),Y)) .
endo

Negative results

Positive results

1. Ex4_4_Luc96b is proved µ-terminating in [Luc96b, Example 4.23] by using Lucas' transformation. The TRS Ex4_4_Luc96b_L:

      f(g(X)) -> f(X)
   

   is terminating (proved with MuTerm):

      Proof of termination for CS-TRS  Ex4_4_Luc96b_L:
   
      [f](X) = X
      [g](X) = X + 1
   

2. The µ-termination of Ex4_4_Luc96b can be proved by using Giesl and Middeldorp's transformation: The TRS Ex4_4_Luc96b_GM:

      a__f(g(X),Y) -> a__f(mark(X),f(g(X),Y))
      mark(f(X1,X2)) -> a__f(mark(X1),X2)
      mark(g(X)) -> g(mark(X))
      a__f(X1,X2) -> f(X1,X2)
   

   is terminating (proved with MuTerm):.
3. The µ-termination of Ex4_4_Luc96b can also be proved by using a polynomial interpretation (computed with MuTerm):

      Proof of termination for CS-TRS  Ex4_4_Luc96b:
   
      [f](X1,X2) = X1
      [g](X) = X + 1
   

4. The µ-termination of Ex4_4_Luc96b can be proved by using CSRPO (computed with MuTerm).
5. The µ-termination of Ex4_4_Luc96b can be proved by using CSDP (computed with MuTerm).